package AI;

import gui.Main;

import java.awt.Point;
import java.io.File;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import javax.swing.tree.DefaultMutableTreeNode;

import world.FieldValues;



public class KnowledgeBase {

	Set<Formula> rules = new HashSet<Formula>();
	Formula infereTemp = new Formula();
	
	public KnowledgeBase() {
		  rules = new HashSet<Formula>();
		  infereTemp = new Formula();
	  }
	  
	public KnowledgeBase(Formula rule) {
		  rules.add(rule);
		  infereTemp = new Formula();
	}
	  
	public KnowledgeBase(Set<Formula> rules) {
		  this.rules.addAll(rules);
		  infereTemp = new Formula();
	}
	
	public Iterator<Formula> returnIterator() {
		return rules.iterator();
	}

	public void addRule(Formula f) {
		rules.add(f);
	}
	
	public void removeRule(Formula f) {
		Iterator<Formula> i = returnIterator();
		while(i.hasNext()) {
			if (i.next().equals(f))
				i.remove();
		}
	}
	
	public void removeLiteral(Literal l) {
		Iterator<Formula> i = returnIterator();
		Formula f = null;
		while (i.hasNext()) {
			f = i.next();
			f.removeLiteral(l, 0);	
			f.removeLiteral(l, 1);
			if(f.isEmpty())
				removeRule(f);
		}		
	}
	
	public boolean findLiteral(Literal l) {
		Iterator<Formula> i = returnIterator();
		Iterator<Literal> j = null;
		Formula f = null;
		while (i.hasNext()) {
			f = i.next();
			j = f.returnIterator();
			while (j.hasNext()) {
				if(j.next().equals(l))
					return true;				
			}
		}
		return false;
	}
	
	public void addToTemp(Literal l) {
		infereTemp.setLiteral(l, 0);
	}
	
	public Formula getTemp() {
		return infereTemp;
	}
	
	public void clearTemp() {
		infereTemp.clearFormula();
	}
	
	public boolean checkCycles(Literal l, Formula f) {
		Iterator<Literal> i = f.returnIterator();
		while (i.hasNext()) {
			if (l.equals(i.next())) {
				return true;
			}
		}
		return false;
	}
	
	public void print() {
		for (Formula f : rules) {
			f.print();
		}
	}
	
	/*public boolean backInference(Literal l, DefaultMutableTreeNode parent) {
		//l.addToTree();
		DefaultMutableTreeNode thisNode = Main.getInstance().getTree().addChild(parent, l.toString());
		Iterator<Formula> i = rules.iterator();
		Iterator<Literal> j = null;		
		Formula f = null;
		Literal temp = null;
		boolean result = true;
		Literal tmp;
		
		//print();
		
		while(i.hasNext()) {
			f = i.next();
			f.print();
			System.out.println("----------");
			if (f.getLiteral()==null) {
				j = f.returnIterator();
				while(j.hasNext()) {
					tmp = j.next();
					if(tmp.equals(l)) {
						// wyświetlanie wyniku na koniec
						thisNode.setUserObject(l.toString() + " = [true]");
						return true;
					}
				}
				j = null;
			} else if (f.getLiteral().equals(l)) {				
				j = f.returnIterator();
				while(j.hasNext()) {
					temp = j.next();
					if (f.getLiteralSet().containsAll(infereTemp.getLiteralSet()) && !infereTemp.getLiteralSet().isEmpty()) {
						result = false;
						break;
					}						
					if(!checkCycles(temp, getTemp())) {					
						addToTemp(temp);
						result = result && backInference(temp,thisNode);
					}
				}
				if (result) {
					// wyświetlanie wyniku na koniec
					thisNode.setUserObject(l.toString() + " = [true]");
					return true;
				} else {
					result = true;
				}				
				j = null;
			}
		}
		// wyświetlanie wyniku na koniec
		thisNode.setUserObject(l.toString() + " = [false]");
		return false;
	}*/
	
	//backInference, ktora na pewno dziala
	public boolean backInference(Literal l, DefaultMutableTreeNode parent) {
		DefaultMutableTreeNode thisNode = Main.getInstance().getTree().addChild(parent, l.toString());
		Iterator<Formula> i = null;
		Iterator<Literal> j = null;		
		Formula f = null;
		Literal temp = null;
		boolean result = true;
		boolean emptyInference = false;
		Literal tmp;
		
		if(!infereTemp.getLiteralSet().contains(l)) {
			addToTemp(l);
		}
		
		//najpierw sprawdza czy poszukiwany literal jest w faktach bazy wiedzy
		//jezeli tak nie wnioskuje dalej
		i = rules.iterator();
		while(i.hasNext()) {
			f = i.next();
			if (f.getLiteral()==null) {
				j = f.returnIterator();
				while(j.hasNext()) {
					tmp = j.next();
					if(tmp.equals(l)) {
						// wyświetlanie wyniku na koniec
						thisNode.setUserObject(l.toString() + " = [true]");
						return true;
					}
				}
			}
		}
		
		//jezeli nie znalazl literalu w faktach to szuka w bazie wiedzy reguly, z ktorej da sie
		//ten literal wywnioskowac
		i = rules.iterator();
		while(i.hasNext()) {
			f = i.next();
			//przeprowadza rekurencyjne wnioskowanie tylko wtedy jezeli znalazl odpowiednia regule,
			//ale tez jezeli wszystkie literaly w tej regule nie sa juz w zbiorze infereTemp
			if (f.getLiteral()!=null && f.getLiteral().equals(l)
					&& !(!infereTemp.getLiteralSet().isEmpty() 
							&& infereTemp.getLiteralSet().containsAll(f.getLiteralSet())) ) {
//							&& f.getLiteralSet().containsAll(infereTemp.getLiteralSet())) ) {
				emptyInference = false;
				j = f.returnIterator();
				while(j.hasNext()) {
					temp = j.next();					
					if(!checkCycles(temp, getTemp())) {					
						addToTemp(temp);						
						result = result && backInference(temp, thisNode);
					}					
				}

			} else {
				//jezeli dany literal nie spelniaja powyzszych warunkow ustawiamy flage, ze nie
				//doszlo do wnioskowania i sprawdzamy kolejna regule w bazie wiedzy
				emptyInference = true;
				continue;
			}
			//jezeli result zwrocil true i nie bylo pustego wnioskowania to wyjdz z metody z true
			if(result && !emptyInference) {
				// wyświetlanie wyniku na koniec
				thisNode.setUserObject(l.toString() + " = [true]");
				return true;
			} else if (i.hasNext()){
				//jezeli nie, ale sa w bazie wiedzy jeszcze jakies reguly to ustaw result na true
				//(dlatego ze jest result && we wnioskowaniu) i testuj nastepna regule
				result = true;
			}
		}
		
		//jezeli po przejsciu calej bazy wiedzy flaga jest true czyli nie bylo zadnej reguly z ktorej
		//moglibysmy wywnioskowac literal l to zwroc false
		if(emptyInference) {
			// wyświetlanie wyniku na koniec
			thisNode.setUserObject(l.toString() + " = [false]");
			return false;			
		} else {
			//jezeli flaga nie byla ustawiona to zwroc to co dal result (de facto zawsze bedzie false,
			//bo gdyby result dal true metoda wrocilaby znacznie wczesniej
			// wyświetlanie wyniku na koniec
			thisNode.setUserObject(l.toString() + " = ["+result+"]");
			return result;
		}
	}
	
	
	//wersja backInference tylko do celow testowania
	/*public boolean backInference(Literal l) {
		Iterator<Formula> i = null;
		Iterator<Literal> j = null;		
		Formula f = null;
		Literal temp = null;
		boolean result = true;
		boolean emptyInference = false;
		Literal tmp;
		
		i = rules.iterator();
		while(i.hasNext()) {
			f = i.next();
			if (f.getLiteral()==null) {
				j = f.returnIterator();
				while(j.hasNext()) {
					tmp = j.next();
					if(tmp.equals(l)) {
						return true;
					}
				}
			}
		}
				
		i = rules.iterator();
		while(i.hasNext()) {
			f = i.next();
			if (f.getLiteral()!=null && f.getLiteral().equals(l)
					&& !(!infereTemp.getLiteralSet().isEmpty() 
							&& f.getLiteralSet().containsAll(infereTemp.getLiteralSet())) ) {
				emptyInference = false;
				j = f.returnIterator();
				while(j.hasNext()) {
					temp = j.next();					
					if(!checkCycles(temp, getTemp())) {					
						addToTemp(temp);						
						result = result && backInference(temp);
					}					
				}

			} else {
				emptyInference = true;
				continue;
			}
			if(result && !emptyInference) {
				return true;
			} else if (i.hasNext()){
				result = true;
			}
		}
		
		if(emptyInference) {
			return false;			
		} else {
			return result;
		}
	}*/
	
	public void showKB() {
		Iterator<Formula> i = returnIterator();
		while (i.hasNext()) {
			i.next().print();
		}
	}
	
	public void isWall(Point p, FieldValues dir) {
		Formula f = new Formula();
		switch (dir) {
		case UP:
			f.setLiteral(new Literal(p, LiteralType.UP), 0);
			f.setLiteral(new Literal(p, LiteralType.BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x, p.y-1), LiteralType.WALL), 1);
			break;
		case RIGHT:
			f.setLiteral(new Literal(p, LiteralType.RIGHT), 0);
			f.setLiteral(new Literal(p, LiteralType.BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x+1, p.y), LiteralType.WALL), 1);
			break;
		case DOWN:
			f.setLiteral(new Literal(p, LiteralType.DOWN), 0);
			f.setLiteral(new Literal(p, LiteralType.BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x, p.y+1), LiteralType.WALL), 1);
			break;
		case LEFT:
			f.setLiteral(new Literal(p, LiteralType.LEFT), 0);
			f.setLiteral(new Literal(p, LiteralType.BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x-1, p.y), LiteralType.WALL), 1);
			break;

		default:
			break;
		}
		
		addRule(f);
	}
	
	public void isDanger(Point p, LiteralType dangerType) {
		LiteralType signalType;
		Formula f = new Formula();
		
		if (dangerType == LiteralType.WUMPUS) {
			signalType = LiteralType.STENCH;
			f.setLiteral(new Literal(new Point(p.x,p.y-1), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x+1,p.y), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x,p.y+1), signalType), 0);
			f.setLiteral(new Literal(p, dangerType), 1);
			addRule(f);
			
			f = new Formula();
			f.setLiteral(new Literal(new Point(p.x,p.y-1), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x+1,p.y), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x-1,p.y), signalType), 0);
			f.setLiteral(new Literal(p, dangerType), 1);
			addRule(f);
			
			f = new Formula();
			f.setLiteral(new Literal(new Point(p.x,p.y-1), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x,p.y+1), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x-1,p.y), signalType), 0);
			f.setLiteral(new Literal(p, dangerType), 1);
			addRule(f);
			
			f = new Formula();
			f.setLiteral(new Literal(new Point(p.x+1,p.y), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x,p.y+1), signalType), 0);
			f.setLiteral(new Literal(new Point(p.x-1,p.y), signalType), 0);
			f.setLiteral(new Literal(p, dangerType), 1);
			addRule(f);
			
			oneWumpus(p);
		} else {
			signalType = LiteralType.BREEZE;
		}		
		
		f = new Formula();
		f.setLiteral(new Literal(p, dangerType), 0);
		f.setLiteral(new Literal(new Point(p.x,p.y-1), signalType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, dangerType), 0);
		f.setLiteral(new Literal(new Point(p.x+1,p.y), signalType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, dangerType), 0);
		f.setLiteral(new Literal(new Point(p.x,p.y+1), signalType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, dangerType), 0);
		f.setLiteral(new Literal(new Point(p.x-1,p.y), signalType), 1);
		addRule(f);
	}
	
	private void noWumpus(Point p) {
		Formula f = new Formula();
		f.setLiteral(new Literal(new Point(p.x,p.y-1), LiteralType.STENCH), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_WUMPUS), 1);
		addRule(f);		
	}
	
	private void oneWumpus(Point p) {
		Formula f; 
		for(int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
			for (int j=0; j<Main.getInstance().getMap().getSize(); ++j){
				if (i == p.x && j == p.y)
					continue;
				f = new Formula();
				f.setLiteral(new Literal(p, LiteralType.WUMPUS), 0);
				f.setLiteral(new Literal(new Point(i,j), LiteralType.NO_WUMPUS), 1);
				addRule(f);
			}
		}
	}
	
	/*public void visitedField(Point p) {
		Formula f = new Formula();
		f.setLiteral(new Literal(p, LiteralType.AGENT), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_WUMPUS), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, LiteralType.AGENT), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_PIT), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, LiteralType.AGENT), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_WALL), 1);
		addRule(f);
	}*/
	
	public void visitedField(Point p) {
		Formula f = new Formula();
		f.setLiteral(new Literal(p, LiteralType.NO_WUMPUS), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_PIT), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_WALL), 0);
		addRule(f);
	}
	
	public void isGold(Point p, boolean is) {
		Formula f = new Formula();
		if (is) {
			f.setLiteral(new Literal(p, LiteralType.GLITTER), 0);
			f.setLiteral(new Literal(new Point(p.x,p.y), LiteralType.GOLD), 1);
			addRule(f);
		} else {
			f.setLiteral(new Literal(p, LiteralType.NO_GLITTER), 0);
			f.setLiteral(new Literal(new Point(p.x,p.y), LiteralType.NO_GOLD), 1);
			addRule(f);
		}
	}
	
	public void noDanger(Point p, LiteralType dangerType) {
		LiteralType signalType;
		if (dangerType == LiteralType.NO_WUMPUS) {
			signalType = LiteralType.NO_STENCH;
		} else {
			signalType = LiteralType.NO_BREEZE;
		}
//		Formula f = new Formula();
//		
//		f = new Formula();
//		f.setLiteral(new Literal(p, dangerType), 0);
//		f.setLiteral(new Literal(new Point(p.x,p.y-1), signalType), 1);
//		addRule(f);
//		
//		f = new Formula();
//		f.setLiteral(new Literal(p, dangerType), 0);
//		f.setLiteral(new Literal(new Point(p.x+1,p.y), signalType), 1);
//		addRule(f);
//		
//		f = new Formula();
//		f.setLiteral(new Literal(p, dangerType), 0);
//		f.setLiteral(new Literal(new Point(p.x,p.y+1), signalType), 1);
//		addRule(f);
//		
//		f = new Formula();
//		f.setLiteral(new Literal(p, dangerType), 0);
//		f.setLiteral(new Literal(new Point(p.x-1,p.y), signalType), 1);
//		addRule(f);
	}
	
	public void noSignal(Point p, LiteralType signalType) {
		LiteralType dangerType;
		if (signalType == LiteralType.NO_STENCH) {
			dangerType = LiteralType.NO_WUMPUS;
		} else {
			dangerType = LiteralType.NO_PIT;
		}
		Formula f = new Formula();
		
		f = new Formula();
		f.setLiteral(new Literal(p, signalType), 0);
		f.setLiteral(new Literal(new Point(p.x,p.y-1), dangerType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, signalType), 0);
		f.setLiteral(new Literal(new Point(p.x+1,p.y), dangerType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, signalType), 0);
		f.setLiteral(new Literal(new Point(p.x,p.y+1), dangerType), 1);
		addRule(f);
		
		f = new Formula();
		f.setLiteral(new Literal(p, signalType), 0);
		f.setLiteral(new Literal(new Point(p.x-1,p.y), dangerType), 1);
		addRule(f);
	}
	
	public void noWall(Point p, FieldValues dir) {
		Formula f = new Formula();
		switch (dir) {
		case UP:
			f.setLiteral(new Literal(p, LiteralType.UP), 0);
			f.setLiteral(new Literal(p, LiteralType.NO_BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x, p.y-1), LiteralType.NO_WALL), 1);
			break;
		case RIGHT:
			f.setLiteral(new Literal(p, LiteralType.RIGHT), 0);
			f.setLiteral(new Literal(p, LiteralType.NO_BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x+1, p.y), LiteralType.NO_WALL), 1);
			break;
		case DOWN:
			f.setLiteral(new Literal(p, LiteralType.DOWN), 0);
			f.setLiteral(new Literal(p, LiteralType.NO_BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x, p.y+1), LiteralType.NO_WALL), 1);
			break;
		case LEFT:
			f.setLiteral(new Literal(p, LiteralType.LEFT), 0);
			f.setLiteral(new Literal(p, LiteralType.NO_BUMP_WALL), 0);
			f.setLiteral(new Literal(new Point(p.x-1, p.y), LiteralType.NO_WALL), 1);
			break;

		default:
			break;
		}
		
		addRule(f);
	}
	
	public void noBumpWall(Point p) {
		Formula f = new Formula();
		f.setLiteral(new Literal(new Point(p.x,p.y-1), LiteralType.NO_WALL), 0);
		f.setLiteral(new Literal(new Point(p.x+1,p.y), LiteralType.NO_WALL), 0);
		f.setLiteral(new Literal(new Point(p.x,p.y+1), LiteralType.NO_WALL), 0);
		f.setLiteral(new Literal(new Point(p.x-1,p.y), LiteralType.NO_WALL), 0);
		f.setLiteral(new Literal(p, LiteralType.NO_BUMP_WALL), 1);
		addRule(f);
	}
	
	public void deadWumpus() {
		Formula f = new Formula();
		
		for(int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
			for (int j=0; j<Main.getInstance().getMap().getSize(); ++j) {
				f.setLiteral(new Literal(new Point(i,j), LiteralType.NO_WUMPUS), 0);
			}
		}		
		addRule(f);
			
		Literal l = null;
		//f = new Formula();
		Iterator<Formula> i = returnIterator();
		Iterator<Literal> j = null;
		while (i.hasNext()) {
			f = i.next();
			if(f.getLiteral()==null) {
				j = f.returnIterator();
				while (j.hasNext()) {
					l = j.next();
					if(l.getType()==LiteralType.STENCH) {
						f.removeLiteral(l, 0);
						j = f.returnIterator();
					}					
				}
				if(f.isEmpty()) {
					removeRule(f);
					i = returnIterator();
				}
			}
			
		}
	}
	
	public void wallEdge(Point p, FieldValues dir) {
		Formula f = new Formula();
		switch (dir) {
		case UP:
			for (int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
				f.setLiteral(new Literal(new Point(i, p.y-1), LiteralType.WALL), 0);
			}
			break;
		case RIGHT:
			for (int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
				f.setLiteral(new Literal(new Point(p.x+1, i), LiteralType.WALL), 0);
			}			break;
		case DOWN:
			for (int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
				f.setLiteral(new Literal(new Point(i, p.y+1), LiteralType.WALL), 0);
			}			break;
		case LEFT:
			for (int i=0; i<Main.getInstance().getMap().getSize(); ++i) {
				f.setLiteral(new Literal(new Point(p.x-1, i), LiteralType.WALL), 0);
			}
			break;

		default:
			break;
		}
		
		addRule(f);
	}
	
	public void coveredHole(Point p, FieldValues fv) {
		Formula f = new Formula();
		Literal l = null;
		LiteralType lt = LiteralType.BREEZE;
		Point pitPoint = null;
		switch (fv) {
		case UP:
			pitPoint = new Point((int)p.getX(),(int)p.getY()-1);
			break;
		case DOWN:
			pitPoint = new Point((int)p.getX(),(int)p.getY()+1);
			break;
		case RIGHT:
			pitPoint = new Point((int)p.getX()+1,(int)p.getY());
			break;
		case LEFT:
			pitPoint = new Point((int)p.getX()-1,(int)p.getY());
			break;
		default:
			break;
		}
		
		Iterator<Formula> i = returnIterator();
		Iterator<Literal> j = null;
		while (i.hasNext()) {
			f = i.next();
			if(f.getLiteral()==null) {
				j = f.returnIterator();
				while (j.hasNext()) {
					l = j.next();
					if(l.equals(new Literal(new Point((int)pitPoint.getX()+1,(int)pitPoint.getY()),lt)) 
							|| l.equals(new Literal(new Point((int)pitPoint.getX()-1,(int)pitPoint.getY()),lt))
							|| l.equals(new Literal(new Point((int)pitPoint.getX(),(int)pitPoint.getY()+1),lt))
							|| l.equals(new Literal(new Point((int)pitPoint.getX(),(int)pitPoint.getY()-1),lt))) {
//					if(l.getType()==LiteralType.STENCH) {
						f.removeLiteral(l, 0);
						j = f.returnIterator();
					}					
				}
				if(f.isEmpty()) {
					removeRule(f);
					i = returnIterator();
				}
			}
			
		}
		
	}
}
